Nuprl Lemma : frame-p-realizable
0,22
postcript
pdf
i
,
x
:Id,
T
:Type,
L
:Knd List. Normal(
T
)
es
.@
i
only events in
L
change
x
:
T
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
ES
,
@
i
only events in
L
change
x
:
T
,
Type
,
Prop
,
x
.
t
(
x
)
,
R
||-
es
.
P
(
es
)
,
x
:
A
.
B
(
x
)
,
es
.
P
(
es
)
,
Id
,
Knd
,
type
List
,
Normal(
T
)
,
@
loc
only events in
L
change
x
:
T
Lemmas
normal-type
wf
,
Knd
wf
,
Id
wf
,
Rframe
wf
,
R-realizes
wf
,
frame-p
wf
,
event
system
wf
,
R-frame-rule
origin
i, x:Id, T:Type, L:Knd List. Normal(T) 
es.@i only events in L change x : T i, x:Id, T:Type, L:Knd List. Normal(T) es.@i only events in L change x : T 
T Qx:A. B(x)
x. t(x)
x:A. B(x)es.P(es)